
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%	Rewriting interface
%%%
%%%	Assumption: compile_mapping/0 already invoked.
rewrite_query(H, B):-
	clear_rewriting_query,
	compute_query_lineage(H,B),
	parse_direct_reachable,
	build_renaming,
	rewrite.






%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%	Bottom-up Enumeration of Predicate Patterns
%%% Assumptions:
%%%   1. edb/1 holds all edbs in the form edb(Pred/Arity).
%%%   2. A set of weakly acyclic tgds already stored in rule(SkolemizedHead, Body, OriginalHead), which
%%%      is usually done via tell_tgd/2.


compile_mapping:-
	compute_pattern_fixpoint,
        build_direct_dependent,
	compute_dependent_closure.




set_pattern_nochange :-
	assert(pattern_nochange_flag).
unset_pattern_nochange :-
	retractall(pattern_nochange_flag).


compute_pattern_fixpoint :-
	initialize,
	repeat,
	    set_pattern_nochange,
	    gen_patterns,
	    pattern_nochange_flag, % succeeds only when fixpoint reached
	!.

initialize :-
	dynamicalize_predicates,
	init_edb_patterns.

dynamicalize_predicates :-
	dynamicalize,
	dyno_egd.

init_edb_patterns :-
	edb(P/N),
	init_edb_pattern(P/N),
	fail.
init_edb_patterns.

init_edb_pattern(Pred/N) :-
	functor(Pattern, Pred, N),
	add_pattern(Pattern).



%%	tries generate new pattern/lineage, always returns true.
%%	fixpoint indicated by nochange_flag.
gen_patterns :-
	rule(H, B, _), % loop through all rules (SkolemizedHead, Body, _)
	gen_pattern_single_rule(H, B),
	unset_pattern_nochange, % On reaching here, surely new pattern/lineage are derived.
	fail.
gen_patterns.

%%	gen_pattern_single_rule(H, B): fails if no new pattern/lineage is generated.
%  an optimization is to assign an ID to each rule, and record only rule ID instead
%  of frozen rule itself.
gen_pattern_single_rule(H, B) :-
	freeze_lineage((H, B),(FH, FB)),
	B,  % this may fail if not unifiable
	try_add_lineage_or_pattern(H, B, (FH, FB)).


try_add_lineage_or_pattern(Pattern, BodyPattern, Rule) :-
	\+ lineage(Pattern, BodyPattern, Rule), % fail if not new lineage
	add_lineage(Pattern, BodyPattern, Rule),
	try_add_pattern(Pattern).

%%	add pattern if not already. Always returns true.
try_add_pattern(Pattern) :-
	(
	  \+ Pattern ->
	  add_pattern(Pattern)
	;   true
	).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%	Backward Reachability %



%%	compute_query_lineage(QueryHead, QueryBody):- find all
%   feasible patterns, for later rewriting
compute_query_lineage(H, B):-
	freeze_lineage((H, B),Rule),
	freeze_pattern(H, FH),
	H = FH, %% unify the head to allow no compound
	B,
	add_query_lineage(H, B, Rule),
	fail.
compute_query_lineage(_,_).



parse_direct_reachable :-
	query_lineage(_, Body, _),
	parse_direct_reachable(Body),
	fail.
parse_direct_reachable.

%%	parse_direct_reachable(+QueryBodyPattern)
%    Given a body pattern, parse all directly reachable predicate patterns
parse_direct_reachable(','(S1, S2)):-
	!,
	parse_direct_reachable(S1),
	parse_direct_reachable(S2).
parse_direct_reachable(S):-
	add_reachable(S).





% build direct dependent-on relationship using tgd lineage.
build_direct_dependent :-
	lineage(HeadPattern, BodyPattern, _),
	parse_dependent(BodyPattern, HeadPattern),
	fail.
build_direct_dependent.

%%	parse dependency from (Body, Head) pairs
parse_dependent(','(S1, S2), HeadPattern):-
	!,
	parse_dependent(S1, HeadPattern),
	parse_dependent(S2, HeadPattern).
parse_dependent(Subgoal, HeadPattern) :-
	add_dependent(HeadPattern, Subgoal).

%% compute transitive closure of dpendent_on/2.
compute_dependent_closure :-
	  (
	    dependent_on(A, B),
	    dependent_on(B, C),
	    \+ dependent_on(A, C)
	  ),
	  assert(dependent_on(A,C)),
	  fail.
compute_dependent_closure.




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%	 Predicate Split


%%	currently only for query reachable predicates. In fact, we can
% do it once for a given set of tgds.
build_renaming :-
	build_renaming_direct_reachable,
	build_renaming_dependent_on.

build_renaming_direct_reachable :-
	query_reachable(P),
	build_rename(P),
	fail.
build_renaming_direct_reachable.

build_renaming_dependent_on :-
	query_reachable(P),
	dependent_on(P, D),
	build_rename(D),
	fail.
build_renaming_dependent_on.

%%  rename(+PatternedPredicate):- try create new predicate for given
%%  pattern.
build_rename(Pattern):-
	(
	  \+ renaming_map(Pattern, _)
	-> record_rename_pattern(Pattern)
	; true
	).
record_rename_pattern(Pattern):-
	functor(Pattern, F, _),
	(
	   is_base(Pattern)
	->   NewPred = F
	;    new_split_predicate(F, NewPred)
	),
	add_renaming(Pattern, NewPred).

is_base(Pattern):-
	functor(Pattern, F, N),
	functor(Test, F, N),
	freeze_pattern(Test, FTest),
	FTest == Pattern.

%%	new_split_predicate(PName, NewFun):- create
% a new functor NewFun using the given predicate name
% and current global count.
new_split_predicate(PredName, Functor) :-
	nextFrozenCount(N),
	concat_atom([PredName,N],'_', Functor).

rewrite:-
	rewrite_query,
	rewrite_tgds.

rewrite_query :-
	query_lineage(PH, PB, (RH,RB)),
	rename_query((PH,PB),(RH,RB)),
	fail.
rewrite_query.


%%	perform rewriting of patterned idbs
rewrite_tgds:-
	renaming_map(Pattern, _),
	lineage(Pattern, PBody, (H, B)),
	rename_query((Pattern,PBody), (H,B)),
	fail.
rewrite_tgds.

%%	rewrite a particular lineage in the form of (Pattern, Rule).
rename_query(Pattern, Rule):-
	melt_pattern(Pattern, MeltedPattern),
	melt_lineage(Rule, MeltedRule),
	MeltedPattern = MeltedRule,
	rename(MeltedRule, RenamedRule),
	record_rule(RenamedRule).

%%	rename a conjunctive query
rename((H, B), (RH, RB)):-
	!,
	rename(H, RH),
	rename(B, RB).
rename(Subgoal, Rewritten):-
	rename_subgoal(Subgoal, Rewritten).



%%	rewrite subgoal using renaming_map/2
rename_subgoal(Subgoal, Rewritten):-
	freeze_pattern(Subgoal, Pattern),
	find_rename(Pattern, Pred),
	rename_subgoal(Subgoal, Pred, Rewritten).
%% rewrite_subgoal(+Subgoal, +Pred, -New): rewrite the subgoal into
%  a function-free one using the given predicate.
rename_subgoal(Subgoal, F, NewSubgoal) :-
	extract_vars(Subgoal, Vars),
	NewSubgoal =.. [F| Vars].

find_rename(Pattern, Pred):-
	renaming_map(Pattern, Pred),
	!.
find_rename(Pattern, F):-
	functor(Pattern, F, _).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%  Data structures:
%%%
:- dynamic lineage/3.
:- dynamic pattern/1.
:- dynamic pattern_nochange_flag/0.
:- dynamic edb/1.
:- dynamic dependent_on/2.




%%	query_lineage(QueryHead, QueryBody): separate from lineage
%  for tgds, since query lineage is volatile while tgds lineage
%  lasts for across queries.
:- dynamic query_lineage/3.
%%	query_reachable(PredicatePattern) : directly reachable patterns
:- dynamic query_reachable/1.
%%	rewritten(Head, Body).
:- dynamic rewritten/2.
:- dynamic renaming_map/2.


%   clear all data structures used in rewriting for
%   tgds in context
%   Note: rule/3 is dealt with by clearKnowledgeBase/0.
clear_rewriting_mapping :-
	clear_lineage,
	clear_patterns,
	clear_flag,
	clear_edb,
	clear_dependent,
	clearKnowledgeBase.

clear_rewriting_query :-
	clear_query_lineage,
	clear_query_reachable,
	clear_renaming,
	clear_rewritten.

clear_flag :-
	unset_pattern_nochange.


tell_edb(P/N) :-
	assert(edb(P/N)).


clear_edb :-
	retractall(edb(_)).





%% add_lineage(HeadPattern, BodyPattern, (RHead,RBody)) :
%% all args should be ground.
add_lineage(HPattern, BPattern, Rule) :-
	assert(lineage(HPattern, BPattern, Rule)).
clear_lineage :-
	retractall(lineage(_,_,_)).



%	add_pattern(+Pattern) : Pattern: a pattern that can be
add_pattern(Pattern) :-
	freeze_pattern(Pattern, Frozen),
	assert(Frozen),
	assert(pattern(Frozen)).

remove_pattern(Pattern) :-
	retractall(pattern(Pattern)),
	retractall(Pattern).


clear_patterns :-
	pattern(Pattern),
	remove_pattern(Pattern),
	fail.
clear_patterns.

add_query_lineage(Head, Body, Rule):-
	(   \+ query_lineage(Head, Body, Rule)
	-> assert(query_lineage(Head, Body, Rule))
	;   true
	).
clear_query_lineage :-
	retractall(query_lineage(_,_,_)).


%	add reachable if not yet recorded.
add_reachable(S) :-
	(   \+ query_reachable(S)
	-> assert(query_reachable(S))
	;   true
	).

clear_query_reachable:-
	retractall(query_reachable(_)).

add_dependent(Pattern, Dependened):-
	(
	  \+ dependent_on(Pattern, Dependened)
	  -> assert(dependent_on(Pattern, Dependened))
	;   true
	).

clear_dependent:-
	retractall(dependent_on(_,_)).
record_rule((Head, Body)):-
	assert(rewritten(Head,Body)).
clear_rewritten:-
	retractall(rewritten(_,_)).


add_renaming(From, To) :-
	assert(renaming_map(From, To)).
clear_renaming :-
	retractall(renaming_map(_, _)).










%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%  Utility subroutines:



tell_rewriting_rule('<-'(Head, Body)):-
	tell_rewriting_rule(Head, Body).
tell_rewriting_rule('->'(Body, Head)):-
	tell_rewriting_rule(Head, Body).
tell_rewriting_rule('<->'(QL, QR)):-
	tell_rewriting_rule(QL, QR),
	tell_rewriting_rule(QR, QL).

tell_rewriting_rule(Head, Body) :-
	skolemize((Head,Body), (NH, NB, _)),
	split_head(NH, NewHeads),
	add_rule_for_rewriting(NewHeads, NB).

add_rule_for_rewriting([H|T], NB) :-
	addRule(H, NB, []), %% the old head field is useless for rewriting.
	add_rule_for_rewriting(T, NB).

add_rule_for_rewriting([], _).

%
%	split a conjunctive query into a list of subgoals
split_head(','(H1, H2), SplitHeads) :-
    !,
    split_head(H1, S1),
    split_head(H2, S2),
    append(S1, S2, SplitHeads).

split_head(Head, [Head]).




%      For lineage, the frozen version retains varaibles identities.
freeze_lineage(Term, Frozen) :-
	freeze_term(Term, Frozen, 1, frozen_var).
melt_lineage(Frozen, Term) :-
	melt_term(Frozen, Term, frozen_var).

%	For patterns, the frozen atom unifies all variables to *
freeze_pattern(Term, Frozen) :-
	copy_term(Term, Frozen),
	term_variables(Frozen, Vs),
	freeze_vars(Vs, *).

%	Unify a list of vars to a given symbol (Sym).
freeze_vars([], _).
freeze_vars([H|T], Sym) :-
	H = Sym,
	freeze_vars(T, Sym).





melt_pattern(Frozen, Melted):-
	melt_pattern(Frozen, Melted, *).%% using the same symbol as freeze_pattern/2

melt_pattern(Sym, _, Sym) :-
	!.

melt_pattern(Atom, Atom, Sym):- %% sure Frozen \== Sym due to previous cut
	atomic(Atom),
	!.

melt_pattern(Frozen, Melted, Sym):-
	compound(Frozen),
	functor(Frozen, F, N),
	functor(Melted, F, N),
	melt_pattern(N, Frozen, Melted, Sym).

melt_pattern(N, F, M, Sym) :-
	N > 0,
	!,
	arg(N, F, ArgF),
	melt_pattern(ArgF, ArgM, Sym),
	arg(N, M, ArgM),
	N1 is N-1,
	melt_pattern(N1, F, M, Sym).

melt_pattern(0, _, _, _).



% extract_vars(Pred, Vs): extract a list of variables in the given Pred
% duplicates are maintained in order.
extract_vars(Var, [Var]) :-
	var(Var),
	!.
extract_vars(Atom, []) :-
	atomic(Atom),
	!.

extract_vars(','(T1, T2), Vs) :-
	!,
	extract_vars(T1, Vs1),
	extract_vars(T2, Vs2),
	append(Vs1, Vs2, Vs).

extract_vars(Term, Vs) :-
	compound(Term),
	!,
	functor(Term, F, N),
	extract_vars(N, Term, Vs).

extract_vars(0, _, []) :-
	!.

extract_vars(N, Term, Vs) :-
	N > 0,
	!,
	arg(N, Term, Arg),
	extract_vars(Arg, VN),
	N1 is N-1,
	extract_vars(N1, Term, Vs1),
	append(Vs1, VN, Vs).








%% Obsolete	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% check_vars(Vs): check whether the argument is a list of variables or simple
% constants.
check_var_double_list([H|T]):-
	check_vars(H),
	check_var_double_list(T).
check_var_double_list([]).

check_vars([H|T]):-
	\+ compound(H),
	check_vars(T).
check_vars([]).

%%   extract_pred(+Query, -ListOfPredicates) : Extract predicates in the given query as a list.
extract_pred(','(Subgoal1, Subgoal2), L) :-
	!,
	extract_pred(Subgoal1, L1),
	extract_pred(Subgoal2, L2),
	append(L1, L2, L).
extract_pred(Subgoal, [R]) :-
	functor(Subgoal, F, N),
	R = F/N.


% walk_query(+Query, +Method, -Result) : template for
% walking a query's subgoals, with Result being a list
% and Method/2 being a predicate of the form Method(+Subgoal, -Output).
% For example, extract_pred can be simulated using walk_qury(Query, find_pred, L).
walk_query(','(Subgoal1, Subgoal2), Method, L) :-
	!,
	walk_query(Subgoal1, Method, L1),
	walk_query(Subgoal2, Method, L2),
	append(L1, L2, L).
walk_query(Subgoal, Method, [R]) :-
	Goal =.. [Method, Subgoal,R],
	call(Goal).
find_pred(Subgoal, P) :-
	functor(Subgoal, F, N),
	P = F/N.



%% lineage_to_pattern(+LineageAtom, -PatternAtom): convert a atom
% frozen as lineage to the version frozen as pattern, i.e., unifying
% all distinct variables.
lineage_to_pattern(Lineage, Pattern):-
	melt_lineage(Lineage, Melted),
	freeze_pattern(Melted, Pattern).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Tests
test_all :-
	test_init_edb_pattern,
	test_freeze_pattern.


test_extract_pred :-
	extract_pred((q(a, f(X)),p(1),pred(X, Y)),  [q/2, p/1, pred/2]).

test_query_walker :-
	walk_query((q(a, f(X)),p(1),pred(X, Y)), find_pred,  [q/2, p/1, pred/2]).




test_init_edb_pattern :-
	init_edb_pattern(emp/3),
	pattern(emp(*, *, *)).



test_freeze_pattern :-
	Original = (emp(f(X), Y), sal(g(f(Y)),Z), addr(Z, W)),
	freeze_pattern(Original, Frozen),
	Frozen = (emp(f(*), *), sal(g(f(*)),*), addr(*, *)).
